$\forall$$A$:Type, $a$:$A$ List, $b$:(\{${\it a@}_{0}$:$A$$\mid$ (${\it a@}_{0}$ $\in$ $a$) \}$\rightarrow$Top). mkfpf($a$;$b$) $\in$ $a$:$A$ fp$\rightarrow$ Top